\documentclass{llncs}

\usepackage{epsfig,amsfonts,latexsym,upref}%,xypic}
\usepackage{graphicx,color,cite,times}
\usepackage{amsmath,amssymb,dsfont,eufrak,mathrsfs}

\usepackage{galois}

\newtheorem{defn}{Definition}
\newenvironment{deff}{\begin{defn} \itshape}{\end{defn}}
\newtheorem{teo}{Theorem}
\newenvironment{teoo}{\begin{teo} \itshape}{\end{teo}}
\newtheorem{es}{Example}
\newenvironment{ess}{\begin{es} \itshape}{\end{es}}
\newtheorem{prop}{Proposition}
\newenvironment{propp}{\begin{prop} \itshape}{\end{prop}}      
\newtheorem{lem}{Lemma}
\newenvironment{lemm}{\begin{lem} \itshape}{\end{lem}}
\newtheorem{cor}{Corollary} 
\newenvironment{corr}{\begin{cor} \itshape}{\end{cor}}


% MACRO

%OK
\def\ok#1{\mbox{\raisebox{0ex}[1ex][1ex]{$#1$}}}



\def \tuple#1{\langle #1 \rangle}

\def\tr{\triangleright}
\def\ra{\rightarrow}
\def\la{\leftarrow}
\def\La{\Leftarrow}
\def\lra{\leftrightarrow}
\def\Ra{\Rightarrow}
\def\Lra{\Leftrightarrow}


\newcommand{\sset}[2]{\left\{~#1  \left |
                    \begin{array}{l}#2\end{array} \right.     \right\}}

\def\grass#1{[\![#1]\!]}

\pagestyle{plain}

\begin{document}

\title{Reversability}

%\author{}
			
%\institute{}


\maketitle

%\begin{abstract} In this paper \dots
%\emph{Keywords:} %\end{abstract}


\section{RCCS}

In~\cite{rccs} the authors present a reversible version of CCS called RCCS. In particular, given a process they allow it to backtrack to any \emph{casually equivalent} past. \\

\begin{tabular}{ll}
CCS\\
$\alpha ::=$ & $a \;|\; \bar{a} \;|\; \tau \;|\; \dots$\\
$P ::=$ & $\mathbf{0} \;|\; \Sigma \alpha_i . P_i \;|\; (P | P) \;|\; (a)P$\\
\end{tabular}\\


\begin{tabular}{ll}
RCCS\\
$m ::=$ & $\tuple{}  \;|\; \tuple{1} \cdot m \;|\; \tuple{2} \cdot m \;|\; \tuple{\ast,\alpha,P} \cdot m \;|\; \tuple{m',\alpha,P} \cdot m$\\
$R ::=$ & $m \tr P \;|\;  (R | R) \;|\; (a)R$\\
\end{tabular}\\

%$m \tr P$ is also called thread.\\

%\noindent 
Let $\grass{P}$ and $\grass{R}$ denote the set of traces of the CCS and RCCS processes.
Let us consider the domain $\tuple{\mathbf{CCS},\sqsubseteq}$ where $P \sqsubseteq Q$ iff $\grass{P} \subseteq \grass{Q}$, and the domain  $\tuple{\mathbf{RCCS},\dot{\sqsubseteq}}$ where $R \sqsubseteq S$ iff $\grass{R} \subseteq \grass{S}$. We can define the following Galois connection:
\[
\mathbf{RCCS} \galois{\alpha}{\gamma} \mathbf{CCS}
\]
where the abstraction function $\alpha: \mathbf{RCCS} \ra \mathbf{CCS}$ is defined as follows:
\begin{itemize}
\item $\alpha(m \tr P) = P$
\item $\alpha(R | R) = \alpha(R) | \alpha(R)$
\item $\alpha((a)R) = (a)\alpha(R)$
\end{itemize}
%
The concretization function $\gamma: \mathbf{CCS} \ra \mathbf{RCCS}$ is defined as follows:
\begin{itemize}
\item $\gamma(P) = m_\top \tr P$ where $m_\top \tr P = \{m \tr P | \mbox{where the threads are pairwise coherent} \}$. Namely, this is the largest set of threads of $P$. [DA CAPIRE E SISTEMARE]
\end{itemize}
observe that:
\begin{itemize}
\item$\alpha$ is monotone: if $R \dot{\sqsubseteq} S$ then it means that all the forward traces of $R$ are also forward traces of $S$ and therefore  $\alpha(R) \sqsubseteq \alpha(S)$.
\item $\gamma$ is monotone.
\item $\gamma \circ \alpha$ is extensive: $\gamma(\alpha(m \tr P)) = m_\top \tr P$ and $m \tr P \;\dot{\sqsubseteq} \; m_\top \tr P$
\item $\alpha \circ \gamma$ is the identity: $\alpha(\gamma(P)) = P$
\end{itemize}


\subsection{Irreversible actions}

Let $I$ be the set of irreversible actions, if $I =\top$ then it means that all actions are irreversible and we have CCS, when $I = \emptyset$ then none of the  actions is irreversible and therefore we have RCCS. Let $\tuple{\mathbf{RCCS}_I,\dot{\sqsubseteq}}$ denote the domain of RCCS processes with $I$ the set of their irreversible actions.
We can define the following Galois connection:
\[
\mathbf{RCCS} \galois{\alpha_I}{\gamma_I} \mathbf{RCCS}_I
\]
where the abstraction function $\alpha_I: \mathbf{RCCS} \ra \mathbf{RCCS}_I$ is defined as follows:
\begin{itemize}
\item $\alpha_I(m \tr P) =  \rho(m) \tr P$
\item $\alpha_I(R | R) = \alpha_I(R) | \alpha_I(R)$
\item $\alpha_I((a)R) = (a)\alpha_I(R)$
\end{itemize}
where
\begin{itemize}
\item $\rho(\tuple{}) = \tuple{}$
\item $\rho(\tuple{1} \cdot m) = \tuple{1} \cdot \rho(m)$
\item $\rho(\tuple{2} \cdot m) = \tuple{2} \cdot \rho(m)$
\item $\rho(\tuple{\ast,a,P} \cdot m) = \tuple{\ast,a,P} \cdot \rho(m)$
\item $\rho(\tuple{\ast,\mathbf{a},P} \cdot m) = \rho(m)$
\end{itemize}
%


\bibliographystyle{abbrv}

\bibliography{biblio}%style{abbrv}
\bibliographystyle{plain}

%\begin{thebibliography}{}

%\end{thebibliography}

%\newpage

\end{document}

